Inference at * 
Iof proof for Lemma can-apply-p-filter:


  T:Type, P:(T), f:(x:T. Dec(P(x))), x:T. (can-apply(p-filter(f);x))  P(x) 

latex

 by ((((UnivCD) 
CollapseTHENA (Auto))) 
CollapseTHEN (RepUR ``can-apply p-filter`` ( 0)))
Co 

latex

Co1: 

Co1: 1. T : Type
Co1: 2. P : T
Co1: 3. f : x:T. Dec(P(x))
Co1: 4. x : T
Co1:   (isl(case f(x) of inl(p) => inl x  | inr(p) => inr p ))  P(x)
Co.

Definitions

, Type, x:AB(x), Dec(P), x(s), f(a), x:A. B(x), p-filter(f), can-apply(f;x), b